\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$),\+
\\[0ex]${\it upd}$:update{-}spec(${\it ds}$;${\it da}$).
\-\\[0ex]msg{-}spec{-}loc(${\it snd}$;$i$)
\\[0ex]$\Rightarrow$ update{-}spec{-}decl(${\it upd}$;${\it ds}$)
\\[0ex]$\Rightarrow$ $\neg$"ecl" $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ R{-}Feasible(\=ecl{-}machine at $i$ with state ecl\+
\\[0ex]
\\[0ex]$A$
\\[0ex]
\\[0ex]state variables ${\it ds}$
\\[0ex]
\\[0ex]actions ${\it da}$
\\[0ex]
\\[0ex]sends ${\it snd}$
\\[0ex]
\\[0ex]updates ${\it upd}$)
\-\\[0ex]$\Rightarrow$ (\=$\forall$$B$:Realizer.\+
\\[0ex]R{-}Feasible($B$)
\\[0ex]$\Rightarrow$ (\=$\forall$$k$$\in$ecl{-}kinds($A$) @ fpf{-}domain(${\it da}$).\+
\\[0ex]isrcv($k$)
\\[0ex]$\Rightarrow$ \=(\=source(lnk($k$)) $=$ $i$ $\in$ Id\+\+
\\[0ex]$\Rightarrow$ Valtype(${\it da}$;$k$) $\subseteq\rho$ R{-}da($B$;destination(lnk($k$)))($k$)?Top)
\-\\[0ex]\& (\=destination(lnk($k$)) $=$ $i$ $\in$ Id\+
\\[0ex]$\Rightarrow$ R{-}da($B$;source(lnk($k$)))($k$)?Void $\subseteq\rho$ ${\it da}$($k$)?Void))
\-\-\-\\[0ex]$\Rightarrow$ R{-}icompat(\=ecl{-}machine at $i$ with state ecl\+
\\[0ex]
\\[0ex]$A$
\\[0ex]
\\[0ex]state variables ${\it ds}$
\\[0ex]
\\[0ex]actions ${\it da}$
\\[0ex]
\\[0ex]sends ${\it snd}$
\\[0ex]
\\[0ex]updates ${\it upd}$;$B$))
\-\-
\end{tabbing}